$\forall$$T$:Type, $R$:($T$$\rightarrow$$T$$\rightarrow\mathbb{P}$), $x$, $z$:$T$. ($x$ $R$\^{}+ $z$) $\Leftarrow\!\Rightarrow$ ($\exists$$y$:$T$. (($x$ $R$ $y$) \& ($y$ ($R$$^{\mbox{\scriptsize $\ast$}}$) $z$)))